/* -*- Mode:Prolog; coding:ISO-8859-1; -*- */


:- use_module(library(clpfd)).


:- multifile test/2.
:- discontiguous test/2.



%Always true, it's used to drive the abductive procedure.
gpr(_, _).




check_vars([]).
          
check_vars([H | T]) :-
        var(H), \+ fd_var(H), !,
        (bb_get_value(stats, true) ->
                increment_stat(variables_found)
         ;
                true                   
         ),
        check_vars(T).


check_vars([_H | T]) :-
        check_vars(T).        




%@  @item link(@var{?InputVariable}, @var{?ListOfCurrentOutputs}, @var{?IndexOfTheLink})
%@  is true when @var{InputVariable} is the @var{IndexOfTheLinkth} member of @var{ListOfCurrentOutputs}, counting the first as
%@  element 1.  

link(TT, InputVariable, ListOfCurrentOutputs, IndexOfTheLink) :- 
        link(TT, InputVariable, ListOfCurrentOutputs, IndexOfTheLink, 1). 

link(TT, InputVariable, [[TT | ListOfCurrentOutputs] | _Others], (N, IndexOfTheLink), N) :- 
        nth1(IndexOfTheLink, ListOfCurrentOutputs, InputVariable). 

link(TT, InputVariable, [_ListOfCurrentOutputs | Others], ForTheNext, N) :- 
        NN is N + 1,
        link(TT, InputVariable, Others, ForTheNext, NN).


%@  @item make_output_list(@var{+CurrentOutputList}, @var{+NewOutputs}, @var{-UpdatedOutputList})
%@  Given a current output list (e.g. [[penguin, V1], [ostrich, V2]] and NewOutputs of the 
%@  type [type1(VAR1), type2(var2), ...] (e.g. [penguin(A), bird(B), penguin(C)]), it produces an updated OutputList
%@  (e.g. [[penguin, V1, A, C], [ostrich, V2], [bird, B]]). 

        test(make_output_list/3, Outcome) :-
                (make_output_list( [[penguin, V1], [ostrich, V2]], [penguin(A), bird(B), penguin(C)], [[penguin, V1, A, C], [ostrich, V2], [bird, B]]) ->
                        Outcome = true ; Outcome = false).
        test(make_output_list/3, Outcome) :-
                (make_output_list( [[penguin, p1], [ostrich, o1]], [penguin(p1), bird(b1), penguin(c1)], [[penguin, p1, dontuseme, c1], [ostrich, o1], [bird, b1]]) ->
                        Outcome = true ; Outcome = false).
        test(make_output_list/3, Outcome) :-
                 (make_output_list([],[bird(b)],[[bird,b]]) -> 
                        Outcome = true ; Outcome = false).


make_output_list([], UnusedNewOutputs, UpdatedOutputList) :-
        make_new_type_output_lists(UnusedNewOutputs, UpdatedOutputList).

make_output_list([[CurrentType | RestHeadCOL] | CurrentOutputList], NewOutputs, [[CurrentType | NodNewListForCurrentType] | UpdatedOutputList]) :-
        get_relevant_arguments(CurrentType, NewOutputs, VariablesToAdd, UnusedNewOutputs), !,
        append(RestHeadCOL, VariablesToAdd, NewListForCurrentType),
        remove_duplicates_with_dontuseme(NewListForCurrentType, NodNewListForCurrentType),
        make_output_list(CurrentOutputList, UnusedNewOutputs, UpdatedOutputList).


make_new_type_output_lists([], []).

make_new_type_output_lists([Output | UnusedNewOutputs], [[Type | AllVarWithSameType] | UpdatedOutputList]) :-
        functor(Output, Type, _),
        get_relevant_arguments(Type,  [Output | UnusedNewOutputs], AllVarWithSameType, Rest),
        make_new_type_output_lists(Rest, UpdatedOutputList).
        


%%test%%
        test(get_relevant_arguments/4, Outcome) :-
                (get_relevant_arguments( penguin,[penguin(V2056),bird(V2058),penguin(V2060)], [V2056, V2060], [bird(V2058)]) ->
                        Outcome = true ; Outcome = false).
        test(get_relevant_arguments/4, Outcome) :-
                (get_relevant_arguments( penguin,[penguin(p1),bird(b1),penguin(V2060)], [p1, V2060], [bird(b1)]) ->
                        Outcome = true ; Outcome = false).
%%%%%%%%

get_relevant_arguments(_CurrentType, [], [], []).

get_relevant_arguments(CurrentType, [H | NewOutputs], [Var | AllVarWithSameType], NextNewOutputs) :-
        H =.. [CurrentType, Var], !,
        get_relevant_arguments(CurrentType, NewOutputs, AllVarWithSameType, NextNewOutputs).        

get_relevant_arguments(CurrentType, [H | NewOutputs], AllVarWithSameType, [H | NextNewOutputs]) :-
        get_relevant_arguments(CurrentType, NewOutputs, AllVarWithSameType, NextNewOutputs).




%@ finishlinks(+Outputs, +OutFromHead, -OutLinkList) :-
%       Given a list of Outputs (with their actual value) accumulated in the rule
%       a list of variables that correspond to output placemarkers in the head OutFromHead
%       it returns a list OutLinkList that associates each index of output in the head. The nf  version
%       DOES NOT force all outputs to be used

%TODO: to implement
%finishlinks(_,  [], []).
%
%finishlinks(Outputs, [H | OutFromHead], [IndexChosenOut | OutLinkList]) :-
%        print('ERROR: TO IMPLEMENT FINISHLINKS'), exit,
%        link(H, Outputs, IndexChosenOut), %It takes a variable from the outputs in the head and it link it to something in the output
%        delete_element(_StillToBind, IndexChosenOut, StillToBindNew),
%        finishlinks(Outputs, StillToBindNew, OutFromHead, OutLinkList).


%finishlinksnf([[nat, 1, 2], [name, anna, dom]], [[nat, X], [name, Y]], [[(1,2)], [(2,2]]).
%finishlinksnf([[nat, 1, 2], [name, anna, dom]], [[nat, X], [name, Y]], [[(1,1)],  [x]).

finishlinksnf(_, [], []).

finishlinksnf(Outputs,  [[Type | H] | OutFromHead], [IC | OutLinkList]):-
        flinside(Type, H, Outputs, IC),  %IC is of the type 
        finishlinksnf(Outputs, OutFromHead, OutLinkList).

flinside(_Type, [], _Outputs, []).
flinside(Type, [H | T], Outputs, [IndexChosenOut | TT]):-
        link(Type, H, Outputs, IndexChosenOut),
        flinside(Type, T, Outputs, TT).
   
%@ verify(+CurrentRule) :-
%       This is where the check on the single rule is performed. TODO: improve

verify(X) :- verify_recall(X), verify_rest(X).

verify_recall(X) :- 
        reverse(X, [(ModeId, _, _) | Rest]),
        (additional_info(recall(ModeId), Recall) ->
                count_mode_in(ModeId, Rest, HowMany),
                (HowMany < Recall ->
                        true
                ;
                        %log('Failing for recall '),
                        %log(X),
                        false
                 )
        ;
                true
        ).

count_mode_in(_ModeId, [(_,_,_)], 0) :- !.
count_mode_in(ModeId, [(ModeId, _, _) | Rest], HowMany) :- !,
        count_mode_in(ModeId, Rest, HM1),
        HowMany is HM1 + 1.
count_mode_in(ModeId, [_ | Rest], HowMany) :-  
        count_mode_in(ModeId, Rest, HowMany).
                                              

verify_rest([_, _]) :- !.

verify_rest(L) :-    
        reverse(L, [A | [B | _OldStuff ]]),
        \+ A = B, !.

verify_rest(L) :-   
		bb_get_value(allow_repetition_of_producers, O22),
		(O22 = true ->
	        reverse(L, [NewStuff | [NewStuff | _OldStuff ]]),
    	    NewStuff = (Id, _, _),
       	 additional_info(outputs_in(Id), LOV),
        	LOV > 0, !
       	;
       		false
       	).



%TODO WORK IN PROGRESS
/*
DOM1: this actually goes in the baductive computation if ordering is true (otherwise we poit in the top theory
something that is always true). Remember: At this point the flattening is always ground.
With the exception of constants. We only allow this if the constants have CLPFD.
Note, this is tricky be careful, because we may constrain these variables and then they get a test like
penguin(X) that unifies to penguin(a). At this point X has clpfd like X #> 3 and X = a. Prolog explodes.
Alternatively we can say we always want ground stuff. Less powerful but easy. 
DOM2: Ok no support for now. When we use this, no clpfd on the type. We can leave it as a builtin.
TODO: declare it as a builtin.
*/
verify_order(_) :-
        \+ bb_get_value(ordering, true), !.     


verify_order([_, _]) :-
        bb_get_value(ordering, true), !.

verify_order(L) :-
        bb_get_value(ordering, true),      
        respects_aspal_order_simple(L), !.
       %nl, write(L), write(' respects total order').

verify_order(L) :-
        bb_get_value(ordering, true),      
        respects_aspal_order(L), !.
        %nl, write(L), write(' uses variables from previous').

verify_order(_L) :-
        %nl, write(L), print('-> Does not respect order!'), 
        fail.

        
respects_aspal_order_simple(L) :- 
        reverse(L, [NewStuff | [BeforeLast | _OldStuff ]]),
        NewStuff @> BeforeLast, !.

respects_aspal_order_simple(L) :- 
        reverse(L, [NewStuff | [NewStuff | _OldStuff ]]),
        NewStuff = (Id, _, _),
        additional_info(outputs_in(Id), LOV),
        LOV > 0.


respects_aspal_order(L) :-
        reverse(L, [NewStuff | [_BeforeLast | OldStuff ]]),
        reverse(OldStuff, OldStuffRO),
        reconstruct_dummy_output_list(OldStuffRO, Dummyoutputlist), !, 
%        write(check_all_links(NewStuff, Dummyoutputlist)),nl,nl,
        check_all_links(NewStuff, Dummyoutputlist).
%        write('How did we get here if it fails').


check_all_links((_,_, Links), Dummyoutputlists) :- !,
        check_all_linksx(Links, Dummyoutputlists), !.
%        write('IT ACTUALLYSUCCEEDS FOR '), write(Links), write(' in list '), write(Dummyoutputlists).

check_all_linksx([], _) :- !, fail.

check_all_linksx([H | T], Dummyoutputlists) :-
%        write('\nChecking '), write(H), write(' in list '), write(Dummyoutputlists),
        link(_, _X, Dummyoutputlists, H), !,
%        write(' It worked!\n Now checking : '),
%        write(T),
        check_all_linksx(T, Dummyoutputlists).

check_all_linksx(_, _).


reconstruct_dummy_output_list([H | OldStuffRO], FinalResult) :-
        H = (FinalId, _, _),
        modename(FinalId, HeadDec),
        arg(1, HeadDec, Schema),
        dissection(Schema, AllArguments, _DissectionedLiteral), 
        generate_vars_and_type_check(AllArguments, _InputVars, _OutputVars, _ConstantVars, _AllVars, TCheckIn, _TCheckC, _TCheckO),
        make_output_list([], TCheckIn, OutputList),
        reconstruct_dummy_output_list(OldStuffRO, OutputList, FinalResult).

reconstruct_dummy_output_list([], FinalResult, FinalResult).

reconstruct_dummy_output_list([B | OldStuffRO], OutputList, FinalResult) :-
        B = (FinalId, _, _),
        modename(FinalId, BodyDec),
        arg(1, BodyDec, Schema),
        dissection(Schema, AllArguments, _DissectionedLiteral),
        generate_vars_and_type_check(AllArguments, _InputVars, _OutputVars, _ConstantVars, _AllVars, _TCheckIn, _TCheckC, TCheckO),
        make_output_list(OutputList, TCheckO, OutputVarsNext),
        reconstruct_dummy_output_list(OldStuffRO, OutputVarsNext, FinalResult).


simulate_outputs(0, []):-!.
simulate_outputs(N, [x | R]) :-   
        N1 is N - 1,
        simulate_outputs(N1, R).
        
        
nat(s(X)) :- nat(X).
nat(0).
        

%Used to check if an input can be used in a comparison over the reals
%real_check()


inffloat(X) :- print('\nMaximised '), print(X),  minimize(X),  print(X), print('done'),nl.
supfloat(X) :- print('\nMinimised '),  print(X), maximize(X),  print(X), print('done'),nl.
